How to realize LSE narrowing
Identifieur interne : 00B360 ( Main/Exploration ); précédent : 00B359; suivant : 00B361How to realize LSE narrowing
Auteurs : Andreas Werner [Allemagne] ; Alexander Bockmayr [Allemagne] ; Stefan Krischer [Allemagne]Source :
- New Generation Computing [ 0288-3635 ] ; 1998-12-01.
English descriptors
Abstract
Abstract: Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In Ref. 3), we introduced the LSE narrowing strategy, which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for the class of arbitrary canonical systems. LSE narrowing detects redundant derivations by reducibility tests. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be tested. In this paper, we show that many of these subterms are identical. We describe how left-to-right basic occurrences can be used to identify and exclude these identical subterms. This way, we can drastically reduce the number of subterms that have to be tested. Based on these theoretical results, we develop an efficient implementation of LSE narrowing.
Url:
DOI: 10.1007/BF03037431
Affiliations:
- Allemagne
- Bade-Wurtemberg, District de Karlsruhe, Rhénanie-Palatinat, Sarre (Land)
- Karlsruhe, Sarrebruck, Trèves (Allemagne)
- Université de Trèves
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001206
- to stream Istex, to step Curation: 001190
- to stream Istex, to step Checkpoint: 002592
- to stream Main, to step Merge: 00BA82
- to stream Main, to step Curation: 00B360
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">How to realize LSE narrowing</title><author><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name></author><author><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name></author><author><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:4CA2DEA226E4DC8DF117715AA2D627DC181ABB52</idno><date when="1998" year="1998">1998</date><idno type="doi">10.1007/BF03037431</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-72VZ459F-D/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001206</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001206</idno><idno type="wicri:Area/Istex/Curation">001190</idno><idno type="wicri:Area/Istex/Checkpoint">002592</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002592</idno><idno type="wicri:doubleKey">0288-3635:1998:Werner A:how:to:realize</idno><idno type="wicri:Area/Main/Merge">00BA82</idno><idno type="wicri:Area/Main/Curation">00B360</idno><idno type="wicri:Area/Main/Exploration">00B360</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">How to realize LSE narrowing</title><author><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Inline Internet Online Dienste GmbH, Vincenz-Prießnitz-Str. 3, D-76131, Karlsruhe</wicri:regionArea><placeName><region type="land" nuts="1">Bade-Wurtemberg</region><region type="district" nuts="2">District de Karlsruhe</region><settlement type="city">Karlsruhe</settlement></placeName></affiliation></author><author><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>MPI Informatik, Im Stadtwald, D-66123, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author><author><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name><affiliation wicri:level="4"><country xml:lang="fr">Allemagne</country><wicri:regionArea>University of Trier, Fachbereich IV-Informatik, D-54286, Trier</wicri:regionArea><orgName type="university">Université de Trèves</orgName><placeName><settlement type="city">Trèves (Allemagne)</settlement><region type="land" nuts="1">Rhénanie-Palatinat</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">New Generation Computing</title><title level="j" type="abbrev">New Gener Comput</title><idno type="ISSN">0288-3635</idno><idno type="eISSN">1882-7055</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Tokyo</pubPlace><date type="published" when="1998-12-01">1998-12-01</date><biblScope unit="volume">16</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="397">397</biblScope><biblScope unit="page" to="433">433</biblScope></imprint><idno type="ISSN">0288-3635</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0288-3635</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>E -Unification</term><term>Implementation</term><term>Logic and Functional Programming</term><term>Narrowing</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In Ref. 3), we introduced the LSE narrowing strategy, which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for the class of arbitrary canonical systems. LSE narrowing detects redundant derivations by reducibility tests. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be tested. In this paper, we show that many of these subterms are identical. We describe how left-to-right basic occurrences can be used to identify and exclude these identical subterms. This way, we can drastically reduce the number of subterms that have to be tested. Based on these theoretical results, we develop an efficient implementation of LSE narrowing.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Bade-Wurtemberg</li><li>District de Karlsruhe</li><li>Rhénanie-Palatinat</li><li>Sarre (Land)</li></region><settlement><li>Karlsruhe</li><li>Sarrebruck</li><li>Trèves (Allemagne)</li></settlement><orgName><li>Université de Trèves</li></orgName></list><tree><country name="Allemagne"><region name="Bade-Wurtemberg"><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name></region><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00B360 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00B360 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:4CA2DEA226E4DC8DF117715AA2D627DC181ABB52
|texte= How to realize LSE narrowing
}}
| This area was generated with Dilib version V0.6.33. |  |